$\forall$$B$:Type, $R$:($B$$\rightarrow$$B$$\rightarrow\mathbb{P}$). one{-}one($B$;$B$;$R$) $\Rightarrow$ ($\forall$$n$:$\mathbb{N}$. one{-}one($B$;$B$;rel\_exp($B$;$R$;$n$)))